Nuprl Definition : component-realizes 11,40

C |- es,in,out.P(es;in;out)
== X:Interface(ds;da;A). let R,Y = (C(X)) in R |-es.es-decl(es;ds;da P(es;[[X]];[[Y]]) 
latex



clarification:

component-realizes{i:l}
component-realizes(dsdaABCes,in,out.P(es;in;out))
== X:Interface(ds;da;A).
== let R,Y = (C(X))
== in
== scheme-realizes{i:l}
== scheme-realizes(Res.(es-decl(es;ds;da P(es;abs-interface(es;X);abs-interface(es;Y)))) 
latex


Definitions[[X]], es-decl(es;ds;da), P  Q, S |-es.P(es), f(a), let x,y = A in B(x;y), Interface(ds;da;A), x:AB(x)
FDL editor aliasescomponent-realizes

origin